constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
Mike Shulman (Shulman 2022) has proposed an interpretation of affine logic for use in constructive mathematics, called the antithesis interpretation.
The motivation here is that in much of constructive mathematics, especially (but not only) in constructive analysis, statements of interest seem to come in pairs, a statement that amounts to a constructive version of a well-known statement from classical mathematics, and a statement that amounts to a constructive version of , and which is equivalent to in classical logic, but which is not the same as in intuitionistic logic (being sometimes stronger, sometimes weaker, sometimes neither, and similarly for vis-a-vis ). For example, if is the claim that some real number is rational, then is
(the conventional meaning of ‘ is rational’ in constructive analysis), while is
(the conventional meaning of ‘ is irrational’ in constructive analysis); here, is the standard apartness relation between real numbers, whose negation is the equality relation . As you can see, the two statements are de Morgan dual to one another, and so are negations of each other in classical logic, but neither is the negation of the other in intuitionistic logic.
That such pairs of statements commonly arise is a truism in constructive mathematics. The point of the antithesis interpretation is that the pair may be derived systematically from a single statement in affine logic. And this is a sound interpretation?, in that any reasoning valid in affine logic (or even linear logic) will be constructively valid for both statements; that is, if in affine (or even linear) logic, then and in intuitionistic logic. Therefore, as long as the reasoning is affine (or even linear), one can prove intuitionistic theorems about both at once.
The antithesis interpretation also explains why there are often both weak and strong versions of (or even sometimes), having especially to do with the interpretation of disjunction. This comes up already in defining what a set is, because of the nature of the equality relation on a set . As in the example about about rational and irrational real numbers, every set should also be equipped with an antithesis inequality relation , and the axioms for this may be derived from the axioms for an equality relation. The transitivity axiom for equality has two obvious interpretations in affine logic, which lead to two different interpretations in intuitionistic logic as axioms for : a weak version (intepreting ) stating (for elements of ) that if , then if , and if ; and a strong version (interpreting ) stating that if , then or . (The weak version really does follow from the strong version because we also automatically have that and can never both be true.) Ultimately, the weak version says only that is an inequality relation on the set , while the strong version says that is an apartness relation.
Since every proposition comes with an antithesis proposition in the antithesis interpretation, the natural notion of a subset is actually a pair of disjoint subsets, leading to a potentially far-reaching reinterpretation of the role of higher-order logic in constructive mathematics, with concepts like a family of collections of subsets becoming a disjoint pair of families of disjoint pairs of collections of disjoint pairs of subsets.
Last revised on September 6, 2024 at 18:19:48. See the history of this page for a list of all contributions to it.